COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	 lispax.lsp[f81,jmc]	ekl axioms for lisp
C00005 00003
C00007 ENDMK
C⊗;
;;; lispax.lsp[f81,jmc]	ekl axioms for lisp

(proof lispax)

(DECL (U u0 u1 u2 u3 v v0 v1 v2 v3 W w0 w1 w2 w3) |ground| variable listp)

(DECL (X Y Z) |GROUND| VARIABLE sEXP)

(DECL (A B C) |GROUND| VARIABLE)

(DECL (PHI) |GROUND→TRUTHVAL| VARIABLE)

(DECL (NNIL) |GROUND| CONsTANT LIsTp)

(DECL (CONs) |GROUND⊗GROUND→GROUND| CONsTANT)

(DECL (CAR CDR) |GROUND→GROUND| CONsTANT)

(DECL (NULL) |GROUND→TRUTHVAL| CONsTANT)

(DECL (LIsTp) |GROUND→TRUTHVAL| CONsTANT)

(DECL (sEXP) |GROUND→TRUTHVAL| CONsTANT)

(AXIOM |∀U.sEXP(U)|)

(AXIOM |∀X U.LIsTp(CONs(X,U))|)

(AXIOM |∀U.NULL(U)≡U=NNIL|)

(AXIOM |∀X U.¬NULL(CONs(X,U))|)

(AXIOM |∀X U.CAR(CONs(X,U))=X|)

(AXIOM |∀X U.CDR(CONs(X,U))=U|)

(AXIOM |∀PHI.PHI(NNIL)∧(∀X U.PHI(U)⊃PHI(CONs(X,U)))⊃(∀U.PHI(U))|)

;;; Common defined functions

(DECL (*) |GROUND⊗GROUND→GROUND| CONsTANT NIL INFIX 840)

(axiom |∀u v.listp(u*v)|)

(AXIOM |∀U V.(U*V)=IF NULL(U) THEN V ELsE CONs(CAR(U),CDR(U)*V)|)

(decl (reverse list1) |ground→ground| constant)

(decl list |ground* → ground| functional)

(axiom |∀x.listp(list(x))|)

(axiom |∀x.list(x) = cons(x,nnil)|)

(axiom |∀x y.listp(list(x,y))|)

(axiom |∀x y.list(x,y) = cons(x,list(y))|)

(axiom |∀x y z.listp(list(x,y,z))|)

(axiom |∀x y z.list(x,y,z) = cons(x,list(y,z))|)

(axiom |∀u.listp(reverse(u))|)

(axiom |∀u.reverse(u) = if null(u) then nnil
else reverse(cdr(u)) * list(car(u))|)

;;; theorems taken as axioms for further proofs

(axiom |∀u v w.(u*v)*w = u*(v*w)|)

(axiom |∀x u v.cons(x,u*v) = cons(x,u)*v|)

(axiom |∀u v.reverse(u*v) = reverse(v)*reverse(u)|)